(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
a__hd(cons(hd(cons(X1963_3, X2964_3)), Y)) →+ a__hd(cons(X1963_3, X2964_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [X1963_3 / hd(cons(X1963_3, X2964_3))].
The result substitution is [Y / X2964_3].
(2) BOUNDS(n^1, INF)